(set-logic QF_ABV)
(set-option :opt.priority lex)
(set-option :opt.maxsat_engine wmax)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const bv_10-0 (_ BitVec 10))
(declare-const v5 Bool)
(declare-const arr--3363461031884464548_-7620948637467430869-0 (Array (_ BitVec 10) Bool))
(declare-const bv_25-0 (_ BitVec 25))
(declare-const arr--3363461031884464548_-3363461031884464548-0 (Array (_ BitVec 10) (_ BitVec 10)))
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const bv_14-0 (_ BitVec 14))
(declare-const arr--3363461031900702423_8644069468530964595-0 (Array (_ BitVec 25) (Array (_ BitVec 10) (_ BitVec 10))))
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const arr--3363461031883382023_-7620948637467430869-0 (Array (_ BitVec 9) Bool))
(declare-const arr--3363461031884464548_8644069468530964595-0 (Array (_ BitVec 10) (Array (_ BitVec 10) (_ BitVec 10))))
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const bv_10-7 (_ BitVec 10))
(declare-const v13 Bool)
(declare-const v14 Bool)
(assert (or v0 (distinct #b1101100111 (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101)) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))))
(assert (or (and v4 v10 v11 v3) v2 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) (and v4 v10 v11 v3) v2))
(assert (or (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101))))
(assert (or (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) v0 (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))))
(assert (or (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v1 v12))
(assert (or v9 (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) (and v4 v10 v11 v3)))
(assert (or (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5)) (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) v12))
(assert (or v12 (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))))
(assert (or (=> v4 v1) (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))))
(assert (or (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1)))
(assert (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (=> v4 v1) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or v13 (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5)) (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0))))
(assert (or v14 (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or v9 (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (distinct #b1101100111 (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101))))
(assert (or v1 (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v14))
(assert (or v12 v8 v0))
(assert (or (=> v4 v1) (and v4 v10 v11 v3) v13))
(assert (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) v0 v1))
(assert (or (=> v4 v1) v12 (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))))
(assert (or v12 v12 v13))
(assert (or (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (distinct #b1101100111 (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101)) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1)))
(assert (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) v9 v2))
(assert (or v7 (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9)))
(assert (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) v9 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))))
(assert (or v13 (and v4 v10 v11 v3) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1)))
(assert (or v9 (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or v7 (=> v4 v1) (=> v4 v1)))
(assert (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) v13 (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101))))
(assert (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or v1 v13 v7))
(assert (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9)))
(assert (or (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) (=> v4 v1) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))))
(assert (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) v2 v8))
(assert (or v14 (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) v7))
(assert (or (and v4 v10 v11 v3) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))))
(assert (or (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (and v4 v10 v11 v3) v0))
(assert (or (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))))
(assert (or (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) v0 v2))
(assert (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) v9 v9))
(assert (or v2 v1 (and v4 v10 v11 v3)))
(assert (or v7 (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v1))
(assert (or v12 v8 (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101)))
(assert (or v8 (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5)) v12))
(assert (or v8 v14 (distinct #b1101100111 (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101) (bvurem (bvnor bv_10-0 bv_10-0) #b1000110101))))
(assert (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) v1))
(assert (or (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) v9))
(assert (or (and v4 v10 v11 v3) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5)) v1))
(assert (or v9 (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) v9))
(assert (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) v1))
(assert (or (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5)) v8))
(assert (or (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5)) v2 (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101)))
(assert (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (=> v4 v1) v8))
(assert (or v9 (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) v12))
(assert (or (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) v2 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or v1 (and v4 v10 v11 v3) v7))
(assert (or (=> v4 v1) (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) v0))
(assert (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) (=> v4 v1)))
(assert (or (and v4 v10 v11 v3) (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (or (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) v0 (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))))
(assert (=> (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) (and v4 v10 v11 v3) v2) (or (and v4 v10 v11 v3) v2 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))))))
(assert (or (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (=> v4 v1) v8) (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) (=> v4 v1))))
(assert (or (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (and v4 v10 v11 v3) v0))
(assert (and (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (=> v4 v1) v8) (or v9 (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))) (or v12 v8 (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101)) (or v7 (=> v4 v1) (=> v4 v1)) (or (=> v4 v1) (and v4 v10 v11 v3) v13) (or (and v4 v10 v11 v3) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))) (or v7 (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v1) (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) v9 v9)))
(assert (and (or v1 (and v4 v10 v11 v3) v7) (or (and v4 v10 v11 v3) v2 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))) (or (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (and v4 v10 v11 v3) v0) (or v1 (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v14) (or (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v1 v12) (or (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) (xor v4 v2 v3 v5 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111))) (= v6 v2 v3 v4 (=> v4 v1) v3) (= v6 v2 v3 v4 (=> v4 v1) v3) v7 v1 v9) (=> v4 v1))))
(assert (=> (and (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (=> v4 v1) v8) (or v9 (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))) (or v12 v8 (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101)) (or v7 (=> v4 v1) (=> v4 v1)) (or (=> v4 v1) (and v4 v10 v11 v3) v13) (or (and v4 v10 v11 v3) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))) (or v7 (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v1) (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) v9 v9)) (or v12 v8 (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101))))
(assert (or (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (=> v4 v1) v8) (or v2 v1 (and v4 v10 v11 v3))))
(assert (or (distinct bv_10-0 (bvsmod #b1000110101 #b1000110101)) v2 (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))))
(assert (=> (and (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (=> v4 v1) v8) (or v9 (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (or v4 (=> v4 v1) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (= v6 v2 v3 v4 (=> v4 v1) v3) v6 (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)))) (or v12 v8 (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101)) (or v7 (=> v4 v1) (=> v4 v1)) (or (=> v4 v1) (and v4 v10 v11 v3) v13) (or (and v4 v10 v11 v3) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) (distinct (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5) (store arr--3363461031884464548_-7620948637467430869-0 bv_10-0 v5))) (or v7 (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1) v1) (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) v9 v9)) (or (select arr--3363461031884464548_-7620948637467430869-0 (bvnor bv_10-0 bv_10-0)) (= ((_ extract 9 1) #b1101100111) ((_ extract 9 1) #b1101100111)) v1)))
(assert (or (or v13 (and v4 v10 v11 v3) (xor v1 v2 v0 v2 v2 v3 v3 v0 v0 v1)) (or (distinct (bvnor bv_10-0 bv_10-0) (bvsmod #b1000110101 #b1000110101) #b1000110101) v2 v8)))
(maximize bv_10-0)
(minimize bv_10-7)
(minimize bv_14-0)
(maximize bv_25-0)
(check-sat)
(exit)
